Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))
k(x, h(x), a) → h(x)
k(f(x), y, x) → f(x)

Q is empty.


↳ QTRS
  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))
k(x, h(x), a) → h(x)
k(f(x), y, x) → f(x)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))
k(x, h(x), a) → h(x)
k(f(x), y, x) → f(x)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

k(x, h(x), a) → h(x)
Used ordering:
Polynomial interpretation [25]:

POL(a) = 2   
POL(f(x1)) = x1   
POL(g(x1)) = x1   
POL(h(x1)) = x1   
POL(k(x1, x2, x3)) = x1 + x2 + x3   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))
k(f(x), y, x) → f(x)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))
k(f(x), y, x) → f(x)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

k(f(x), y, x) → f(x)
Used ordering:
Polynomial interpretation [25]:

POL(a) = 0   
POL(f(x1)) = x1   
POL(g(x1)) = 2·x1   
POL(h(x1)) = x1   
POL(k(x1, x2, x3)) = 1 + 2·x1 + x2 + 2·x3   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence
            ↳ QTRS
              ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))

The set Q consists of the following terms:

f(a)
h(g(x0))


Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F(a) → H(a)
H(g(x)) → H(f(x))
H(g(x)) → F(x)

The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))

The set Q consists of the following terms:

f(a)
h(g(x0))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

F(a) → H(a)
H(g(x)) → H(f(x))
H(g(x)) → F(x)

The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))

The set Q consists of the following terms:

f(a)
h(g(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ QDP
                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

H(g(x)) → H(f(x))

The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))

The set Q consists of the following terms:

f(a)
h(g(x0))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ QDP
                      ↳ UsableRulesProof
                        ↳ QDP
                          ↳ RFCMatchBoundsDPProof

Q DP problem:
The TRS P consists of the following rules:

H(g(x)) → H(f(x))

The TRS R consists of the following rules:

f(a) → g(h(a))

The set Q consists of the following terms:

f(a)
h(g(x0))

We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 1.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:

H(g(x)) → H(f(x))

To find matches we regarded all rules of R and P:

f(a) → g(h(a))
H(g(x)) → H(f(x))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

40, 41, 42, 43, 44, 45

Node 40 is start node and node 41 is final node.

Those nodes are connect through the following edges: